from XSY.DEVS.ReachGen import *
from XSY.Graph.KernelDAG import *
import time
from datetime import datetime
from XSY.Set.Interval import *
import pkg_resources

class VeriEngine:
   '''graph-based verification engine'''
   def __init__(self, md, X, checkdeadlockCB, checklivenessCB):
      '''constructor'''
      print str(datetime.now())     
      print 'XSY version %s'%pkg_resources.get_distribution("XSY").version

      self.deve = md
      answer = 'c'
      while( answer != 'y' and answer != 'n' ):
         answer = raw_input("do you want to filter out infinite lifespan? 'y', 'n'>?")

      if answer == 'y':
         TID.inf_trim_out = True
      else:
         TID.inf_trim_out = False

      print 'Wait... while creating the reachability graph....'
      stime = time.clock()
      self.Reach = Reachability(md,X)
      self.checkdeadlockCB = checkdeadlockCB
      self.CheckLivenessCB = checklivenessCB
      self.KDAG_RG = None
      print 'Reachability Graph has been created.'
      print 'elapsed time = %s'%(time.clock() - stime)

   def CheckSafety(self):
      '''check if there exists v in Reach.G.V: DeadLockCB(v) == True'''
      stime = time.clock()
      if self.checkdeadlockCB == None:
         print 'checking deadlock function is NOT defined'
      elif self.checkdeadlockCB(self.Reach.G): 
         print 'System is unsafe!'
      else:
         print 'System is safe!'
      print 'elapsed time = %s'%(time.clock() - stime)

   def CheckLiveness(self):
      '''check if the system is alive'''
      stime = time.clock()
      if self.KDAG_RG == None:
         self.KDAG_RG = KernelDAG(self.Reach.G)
      if self.CheckLivenessCB == None:
	 print 'check liveness function is NOT defined'
      elif self.CheckLivenessCB(self.KDAG_RG):
         print 'System is alive!'
      else:
         print 'System is not alive!'
      print 'elapsed time = %s'%(time.clock() - stime)

   def PrintRepository(self):
      '''print repository of memory'''
      self.Reach.PrintRepository()

   def display_menu(self):
      '''display menu'''
      print '\nprint R(G), print (k)ernelRG, print (r)epo, (s)afety,  (l)iveness, e(x)it'

   def runtimeInteractiveMenu(self):
      '''Verification Runtime Interative Menu'''
      while True:
         self.display_menu()
         s = raw_input()
         if (s == 'g' or s == 'G' or s == 'print RG'):
            print str(datetime.now())
            print self.Reach
         elif (s == 'k' or s == 'K' or s == 'print kernelRG'):
            print str(datetime.now())
            if self.KDAG_RG == None:
               self.KDAG_RG = KernelDAG(self.Reach.G)
            self.KDAG_RG.printG()
         elif (s == 'r' or s == 'R'):
            self.PrintRepository()
         elif (s == 's' or s == 'safety'):
            print str(datetime.now())
            self.CheckSafety()
         elif (s == 'l' or s == 'liveness'):
            print str(datetime.now())
            self.CheckLiveness()
         elif (s == 'x' or s == 'exit'):
            print str(datetime.now())
            break 
         else:
            print 'Invalid menu'

if __name__ == '__main__':
   print 'VeriEngine.py'
